The availability of multiple processing units in current computing hardware, introduced by new multi-core processor architectures, provides computing power that cannot be exploited by programs using traditional algorithms and data structures. In previous single-processor architectures, only one thread of execution could be executing at any given time, thus preventing two threads from operating on the same data structure at the same time was relatively easy to avoid data corruption in the data structure, while having a minimal performance impact.
With multi-core processors, however multiple threads may be programmed by computer-executable code (or simply “code”) to run concurrently on the different processing units (or “cores”). Preventing their concurrent operation on a data structure is not an efficient way to avoid data corruption, because resources (i.e. cores in the multi-core processor) are wasted if, at most, only one thread may run. New algorithms are needed to enable multiple threads to access the data structures concurrently. This means rewriting the code implementing the data structures. The new code is harder to verify for correctness, because of the inherently greater complexity of considering multiple concurrent execution paths instead of a single execution path.
Few verifiers that verify the correctness of parallel algorithms exist and all of them either merely verify very simple properties of a data structure or a data structure that only have simple properties, (see e.g., Vafeiadis, Shape-value Abstraction for Verifying Linearizability, VMCIA 2009, and Fraser, Practical lock-freedom, Technical Report, University of Cambridge, 2004). As a result, automated tools, such as correctness verifiers, are needed to help a developer evaluate the correctness of written code and to improve productivity, as well as improving the quality and reliability of the data structure itself.
In addition, verifying the correctness of a parallel algorithm has been historically viewed as a complex operation that is computationally intensive. Consequently, performing any analysis on the execution of an algorithm has been limited, if performed at all. For example, given all the possible atomic operations (i.e., operations irreducible to some other visible sub-operations) that may be performed upon a data structure, a software test program will execute these operations repeatedly, and in some random order, using multiple concurrent threads. The output of the test program is a history of all the atomic operations performed and their results. In general, a longer test program history includes a richer combination of operations (e.g., a greater number of overlapping operations), and accordingly improves the accuracy of the verifier. Using traditional verification methods, however, implies that longer histories required greater computational requirements. Thus there is a further need for an efficient verifier: one whose computational requirements do not grow excessively with the length of the history.